X:Type, eq:EqDecider(X), f, g:x:X fp Type. g  f  {x:X. f(x)?Top  g(x)?Top} 

latex

Definitions	{T}, EqDecider(T), f(x)?z, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), x. t(x), f(x), , Prop, b, b, Top, f  g, x:A. B(x), A & B, t  T, A, P  Q, False
Lemmas	assert wf, not wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, fpf-ap wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, fpf-cap wf, top wf, deq wf, fpf wf, fpf-sub wf